
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{BoolEval} (\coqdocvar{s}: \coqdocvar{State}) : \coqdocvar{BoolExp} \ensuremath{\rightarrow} \coqdocvar{Bool} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_lit} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{b}:\coqdocvar{ITs.Bool}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_lit} \coqdocvar{b}) \coqdocvar{b}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_id}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{i}:\coqdocvar{Id})(\coqdocvar{b}:\coqdocvar{Bool}),\coqdoceol
\coqdocindent{3.50em}
\coqdocvar{s} \coqdocvar{i} = \coqdocvar{Some} (\coqdocvar{bool\_val} \coqdocvar{b}) \ensuremath{\rightarrow}  \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_id} \coqdocvar{i}) \coqdocvar{b}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_eq}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp})(\coqdocvar{n1} \coqdocvar{n2}: \coqdocvar{Integer}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_eq} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_eq} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_lt}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp})(\coqdocvar{n1} \coqdocvar{n2}: \coqdocvar{Integer}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_lt} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_lt} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_le}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp})(\coqdocvar{n1} \coqdocvar{n2}: \coqdocvar{Integer}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_le} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_le} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_gt}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp})(\coqdocvar{n1} \coqdocvar{n2}: \coqdocvar{Integer}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_gt} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_gt} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{0.50em}
\ensuremath{|} \coqdocvar{bool\_eval\_gtb}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ByteExp})(\coqdocvar{n1} \coqdocvar{n2}: \coqdocvar{Byte}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e1} (\coqdocvar{Some} \coqdocvar{n1}) \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e2} (\coqdocvar{Some} \coqdocvar{n2}) \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_gtb} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{byte\_gt} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocindent{0.50em}
\coqdoceol
\coqdocindent{0.50em}
\ensuremath{|} \coqdocvar{bool\_eval\_eqb}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ByteExp})(\coqdocvar{n1} \coqdocvar{n2}: \coqdocvar{Byte}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e1} (\coqdocvar{Some} \coqdocvar{n1}) \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e2} (\coqdocvar{Some} \coqdocvar{n2}) \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_eqb} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{byte\_eq} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_ge}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ArithExp})(\coqdocvar{n1} \coqdocvar{n2}: \coqdocvar{Integer}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{n1} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{n2} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_ge} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{int\_ge} \coqdocvar{n1} \coqdocvar{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_not} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1}: \coqdocvar{BoolExp})(\coqdocvar{b1}: \coqdocvar{Bool}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{b1} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_not} \coqdocvar{e1}) (\coqdocvar{bool\_not} \coqdocvar{b1})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_and} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{BoolExp})(\coqdocvar{b1} \coqdocvar{b2}: \coqdocvar{Bool}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{b1} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{b2} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_and} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{bool\_and} \coqdocvar{b1} \coqdocvar{b2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_eval\_or}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{BoolExp})(\coqdocvar{b1} \coqdocvar{b2}: \coqdocvar{Bool}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{s} \coqdocvar{e1} \coqdocvar{b1} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} \coqdocvar{e2} \coqdocvar{b2} \ensuremath{\rightarrow} \coqdocvar{BoolEval} \coqdocvar{s} (\coqdocvar{bool\_exp\_or} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{bool\_or} \coqdocvar{b1} \coqdocvar{b2})\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}